module MeteoCal

//SIGNATURES

sig User {
	notification: set Notification,
	calendar: one Calendar,
	createdEvent: set Event
} 

abstract sig Notification {
	referredTo: one Event
}

sig InvitationNotification extends Notification {
}

sig BadWeatherNotification extends Notification {
}

sig DeleteEventNotification extends Notification {
}

sig ModifyEventNotification extends Notification {
}

sig Event {
	invitation: set Invitation,
	forecast: lone WeatherForecast
}

sig WeatherForecast {
} 

sig Invitation {
	invited: one User
} 

sig AcceptedInvitation extends Invitation {
}

sig Calendar {
	partecipation: set AcceptedInvitation
}

//FACTS

fact userProperties {
	//Each event has one and only one creator
	all e: Event | e in User.createdEvent
	all disj u1, u2: User | u1.createdEvent & u2.createdEvent = none
	//Each notification has one and only one owner
	all n: Notification | n in User.notification
	all disj u1,u2: User | u1.notification & u2.notification = none
	//Each calendar has one and only one owner
	all c: Calendar | c in User.calendar
	all disj u1,u2: User | u1.calendar & u2.calendar = none
}

fact eventProperties {
	//Each invitation is referred to one and only one event
	all i: Invitation | i in Event.invitation
	all disj e1,e2: Event | e1.invitation & e2.invitation = none
	//Each weather forecast is referred to one and only one event
	all w: WeatherForecast | w in Event.forecast
	all disj e1,e2: Event | e1.forecast & e2.forecast = none
	//Each event has always his creator as participant
	all u: User, e: u.createdEvent |  u in acceptedInvitations[e].invited
}

fact invitationProperties {
	//Cannot be two invitations referred to the same event and the same user
	all e: Event,  disj i1,i2: e.invitation | i1.invited != i2.invited
}

fact calendarProperties {
	//A calendar contains only and all the accepted invitation of the owner
	all u: User | u.calendar.partecipation = acceptedInvitations[u]
}

fact notificationProperties {
	/*An invitation notification can not be owned by users who partecipate
	 to the event referred by the notification*/
	all u: User, n: invitationFilter[u.notification] | n.referredTo not in partecipateTo[u]
	/*An invitation notification referred to an event can not be owned by a not-invited user
	to that event*/
	all u: User, e: Event | #notAcceptedInvitation[u,e] >= #invitationNotification[u,e]
	//Cannot be two invitation notifications referred to the same event of the same user
	all u: User, disj n1, n2: invitationFilter[u.notification] | n1.referredTo != n2.referredTo
	/*A bad weather notification, a delete event notification or a modify event
	notification can be only owned by users who partecipate to the event referred by the notification*/
	all u: User, n: badWeatherFilter[u.notification] | n.referredTo in partecipateTo[u]
	all u: User, n: modifyEventFilter[u.notification] | n.referredTo in partecipateTo[u]
	all u: User, n: deleteEventFilter[u.notification] | n.referredTo in partecipateTo[u]
	/*A delete event notification or a modify event notification can not be owned by the creator of
	 the event referred by the notification*/
	all u: User, n: modifyEventFilter[u.notification] | n.referredTo not in u.createdEvent
	all u: User, n: deleteEventFilter[u.notification] | n.referredTo not in u.createdEvent
	/*Not more than a bad weather notification for an event can be associated to an user and
	not more than a delete event notification for an event can be associated to an user*/
	all u: User, disj n1, n2: badWeatherFilter[u.notification] | n1.referredTo != n2.referredTo
	all u: User, disj n1, n2: deleteEventFilter[u.notification] | n1.referredTo != n2.referredTo
	//A bad weather notification can be associated only to an event that has a weather forecast yet
	all b: BadWeatherNotification | #b.referredTo.forecast = 1
}

//FUNCTIONS

//get all AcceptedInvitation for an Event
fun acceptedInvitations [e: Event] : set AcceptedInvitation {
	e.invitation & AcceptedInvitation
}
//get all AcceptedInvitation for an User
fun acceptedInvitations [u: User] : set AcceptedInvitation {
	{ai: AcceptedInvitation | ai.invited = u}
}
//get at most one Invitation, not accepted, for an User and an Event
fun notAcceptedInvitation [u: User, e: Event] : lone Invitation {
	{i: Invitation | i not in AcceptedInvitation and i.invited = u and i in e.invitation}
}
//get at most one InvitationNotification for an User and an Event
fun invitationNotification [u: User, e: Event] : lone InvitationNotification {
	{i: InvitationNotification | i.referredTo = e and i in u.notification}
}
//get all Event in which an User participate in
fun partecipateTo [u: User] : set Event {
	{e: Event | u in acceptedInvitations[e].invited}
}

fun invitationFilter [n: Notification] : lone InvitationNotification {
	n & InvitationNotification
}

fun badWeatherFilter [n: Notification] : lone BadWeatherNotification {
	n & BadWeatherNotification
}

fun modifyEventFilter [n: Notification] : lone ModifyEventNotification {
	n & ModifyEventNotification
}

fun deleteEventFilter [n: Notification] : lone DeleteEventNotification {
	n & DeleteEventNotification
}

//ASSERTIONS 
assert numberInvitationNotifications {
	//For each event, the number of invitation not will be equal or less the number of invitations
	all e: Event | #{i: InvitationNotification | i.referredTo = e}<=#(e.invitation)
}

check numberInvitationNotifications

assert numberBadWeatherNotifications {
	//For each event, the number of bad weather not. will be equal or less the number of participants
	all e: Event | #{i: BadWeatherNotification | i.referredTo = e}
		<=#(acceptedInvitations[e])
}

check numberBadWeatherNotifications

assert numberInvitations1 {
	//The number of invitations will be always equal or greater the number of events
	#Invitation >= #Event
}

check numberInvitations1

assert numberInvitations2 {
	//The number of invitations will be always equal or greater the number of invitation notifications
	#Invitation >= #InvitationNotification
}

check numberInvitations2

assert disjInvitationsInCalendars {
	//Two calendars will never contains the same accepted invitation
	all disj c1, c2: Calendar | c1.partecipation & c2.partecipation = none
}

check disjInvitationsInCalendars

assert notReferencedAcceptedInvitations {
	//Each accepted invitation will be always referenced in a calendar
	no ai: AcceptedInvitation | ai not in Calendar.partecipation 
}

check notReferencedAcceptedInvitations

assert createdEventInOwnCalendar {
	//All organized events of an user will be always in his calendar
	all u: User, ai: acceptedInvitations[u] | ai in u.calendar.partecipation
}

check createdEventInOwnCalendar

assert notificationsWithEmptyCalendar {
	//If an user has a notification and an empty calendar, the notification can be only
	//invitation or delete event
	all u:{u: User | u.calendar.partecipation = none}, n: u.notification
	| n in InvitationNotification or n in DeleteEventNotification
}

check notificationsWithEmptyCalendar

//PREDICATES
pred show() {}
run show for 3

pred  showEvents {
	#Event=0
}
run showEvents for 3

pred showNotifications {
	#Notification>4
}
run showNotifications for 5 but 1 Event, 2 User

